i:Id, X:Type, p:FinProbSpace, x0:X, P:(X).
Normal(X)  (preinit1R{x:ut2, a:ut2}(i; X; p; x0; P)  Realizer) 

latex

Definitions	False, A, A  B, P & Q, tt, if b then t else f fi , Top, x. t(x), s.x, preinit1R{$x:ut2, $a:ut2}(i; X; p; x0; P), t  T, P  Q, FinProbSpace, x:A. B(x), i  j < k, {i..j}, , x(s), State(ds), Normal(T), S  T
Lemmas	l member wf, qle wf, l all wf2, int inc rationals, int seg wf, select wf, length wf1, qsum wf, rationals wf, bool wf, normal-type wf, Rinit wf, subtype rel self, eqof eq btrue, id-deq wf, fpf-cap-single, Id wf, fpf-single wf, Rpre wf, Rlist wf